Дисер Феликса Веллена

Море новостей. Во-первых чтобы конструтивно бандлы смоделировать и что-то "посчитать", то посчитать можно только Структурные группы aka Covering Spaces и G-structures, на смоделированых через фломальные étale мапы многообразиях. Так можно смоделировать векторные бандлы и посчитать ихние группы автоморфизмов. Бывает так, что и сам слой F является группой афтоморфизмов. Так вот étale мапы моделируется через интересную штуку — модалити, она есть в конце первой части HoTT, но не испольузется дальше в книге нигде. Бандлы — это вообще самая главная часть алг. топологии, есть в каждом учебнике, можно сравнить определения, но самое интересное — это PhD Феликса Веллена где формализируется на Агде то, про что я сейчас рассказал. Чтобы вы не рылысь в его исходниках я выдер только эти определения, еще там есть 4 равнозначных определения расслоеных пространств, определение модальностей, étale морфизмов на них, многообразий на этале морфизмах, определение G-структуры на Автоморфизмах и фундаментальный инфинити групоид в виде индуктивного типа Майкла Шульмана. Вес это я занимает 500 строчек на Агде Bundle.agda Нашел еще классные слайды Favonia (к которому обращается Роберт Харпер в своих лекциях 15-819) https://www.math.ias.edu/~favonia/files/cover-crm2013-slides.pdf которые показывают, что G-структыры эквивалентны Накрывающим Пространствам.

TOC

Prelude
Path types
Abstract homogeneous structure
Shape (fundamental infinity Groupoid)
Surjections
Pullback
Image
Étale Maps
Automorphism
Manifold
G-sets (Covering Spaces)
Fiber Bundle (4 definitions)

[1]. Felix Wellen. Formalizing Cartan Geometry in Modal Homotopy Type Theory